Termination w.r.t. Q proof of TRS/AProVELiveness6.4.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

top1(free(x), y) → top2(check(new(x)), y)
top1(free(x), y) → top2(new(x), check(y))
top1(free(x), y) → top2(check(x), new(y))
top1(free(x), y) → top2(x, check(new(y)))
top2(x, free(y)) → top1(check(new(x)), y)
top2(x, free(y)) → top1(new(x), check(y))
top2(x, free(y)) → top1(check(x), new(y))
top2(x, free(y)) → top1(x, check(new(y)))
new(free(x)) → free(new(x))
old(free(x)) → free(old(x))
new(serve) → free(serve)
old(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)

Q is empty.

↳ QTRS

Q restricted rewrite system:
The TRS R consists of the following rules:

top1(free(x), y) → top2(check(new(x)), y)
top1(free(x), y) → top2(new(x), check(y))
top1(free(x), y) → top2(check(x), new(y))
top1(free(x), y) → top2(x, check(new(y)))
top2(x, free(y)) → top1(check(new(x)), y)
top2(x, free(y)) → top1(new(x), check(y))
top2(x, free(y)) → top1(check(x), new(y))
top2(x, free(y)) → top1(x, check(new(y)))
new(free(x)) → free(new(x))
old(free(x)) → free(old(x))
new(serve) → free(serve)
old(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)

Q is empty.